\section{Extensibility by Example: the Integration of SCC}
\label{sec.extend}

In this section we present a brief overview of 
the steps undergone to integrate SCC in MFE.
In order to take as much advantage as possible
of the infrastructure offered by MFE, some classes offered by MFE
such as {\tt Tool} and {\tt Proof}
are specialized with new attributes and behavior specific to SCC. In this way,
SCC inherits the behavior defined already for these classes in MFE.
Internal messages defining SCC's public interface
are created and the rewrite rules defining SCC's behavior
are updated so they fit into MFE's message passing interaction mechanism.
Also, the controller object is modified 
to account for SCC in the object-based configuration of 
the formal environment.

\subsection{SCC Proof Objects}

An SCC proof object is an instance of class {\tt SCCProof},
which is a subclass of {\tt Proof}:

\begin{small}
\begin{verbatim}
  class SCCProof | sc-result : SCCResult,
                   terminating : 3Bool,
                   sort-dec : 3Bool,
                   sound : Bool,
                   complete : Bool,
                   trusted : Bool .
  subclass SCCProof < Proof .
\end{verbatim}
\end{small}
%
Attribute {\tt sc-result} registers the sufficient completeness
result of sort {\tt SCCResult}.
If the emptiness test is successful, it holds the
value {\tt empty}; if it is unsuccessful, it
holds a counter-example for sufficient completeness. A counter-example
for sufficient completeness is a ground irreducible term that does
not belong to the subsignature of constructors. Sort {\tt Bool} is
Maude's predefined sort for Boolean values and operations,
and sort {\tt 3Bool} is an extension
of sort {\tt Bool} with a third ``undefined'' value.

Ground termination and ground sort-decreasingness
are assumed in SCC's stand-alone version. 
An SCC proof object in MFE registers the ground
termination and ground sort-decreasingness status of its associated 
module in the three-valued attributes {\tt termi\-nating} and {\tt sort-dec}, respectively,
so that it can be checked whether these assumptions hold (indicated by value {\tt true}),
do not hold (indicated by value {\tt false}), or have not been submitted (indicated
by value {\tt maybe}).
Thanks to
the interoperability offered by MFE and as explained 
in Section~\ref{sec.tools}, 
there are tools in MFE that can 
check for ground termination and ground sort-decreasingness of Maude
specifications. Therefore, SCC proof objects
can always submit these checks to the corresponding tools.

In some situations, some SCC's requirements such as left-linearity
of equations can be relaxed. For instance, if the emptiness check is successful
when ignoring the non left-linear equations in a Maude module, then 
this module is sufficiently complete with all its equations.
However, a counter-example to the sufficient completeness in the
reduced module is not necessarily a sufficient completeness counter-example 
for the module with all its equations.
SCC offers checks for these two properties and, in MFE, 
SCC proof object registers the information with Boolean attributes 
{\tt sound} and {\tt complete}.
SCC proof objects define the Boolean valued
attribute {\tt trusted} for supporting a ``trust'' command for sufficient completeness proofs.
This is useful for dealing with modules that are not supported by SCC or for sufficient completeness
proofs that are obtained outside SCC.

\subsection{The SCC Tool Object}

The SCC tool object is an instance of class {\tt SCCTool}, which is
a subclass of MFE's {\tt Tool}. 
Class {\tt SCCTool} does not declare any new attributes.

\begin{small}
\begin{verbatim}
  class SCCTool .
  subclass SCCTool < Tool .
\end{verbatim}
\end{small}
%
The functional module {\tt SCC-SIGN}
defines the grammar
of the user commands supported by the SCC tool object.
These are the commands available from SCC's stand-alone version
in addition to a new one for showing the state of {\tt SCCProof} 
objects.

\begin{small}
\begin{verbatim}
fmod SCC-SIGN is
  including FULL-MAUDE-SIGN .
  op scc_. : @ModExp@ -> @Command@ .
  op submit . : -> @Command@ .
  op trust . : -> @Command@ .
  op show state . : -> @Command@ .
  op SCC help . : -> @Command@ .
  ...
endfm
\end{verbatim}
\end{small}
%
The command {\tt (scc $MN$.)} checks the sufficient
completeness of module with name {\it MN}.
The command {\tt (submit .)}
submits the termination and sort-decreasingness
proof obligations to the corresponding tools in MFE
for the active SCC proof object, if any.
The command {\tt (trust .)} trusts the sufficient
completeness proof for the active SCC proof object, if any.
The command {\tt (show state .)} displays the state of each SCC
proof object, and
command {\tt (SCC help .)} displays the help menu of Maude's SCC.

Two bodies for internal messages are defined. Namely, a message body
for checking sufficient completeness and a message body
for acknowledging that a module is sufficiently
complete. The latter type of message is only created
when the sufficient completeness check has been successful, and the termination
and sort-decreasingness assumptions have been checked.

\begin{small}
\begin{verbatim}
  op check sc_ : Module -> MFEMsgBody .
  op module_is sufficiently complete : Module -> MFEMsgBody .
\end{verbatim}
\end{small}
%
Observe that command \verb~(scc _.)~ and internal message
body \verb~check sc_~ refer to the same functionality
offered by the SCC tool object, but with different inputs:
the former takes a
module expression as input, while the latter 
takes a {module} as input.
Regardless of this typing difference, 
it is convenient to have exactly one entry point
for commands referring to the same functionality. On the
one hand it facilitates source code maintainability
and debugging. On the other hand, it helps to avoid
repetition of significant amounts of source code.
To address this issue, the SCC tool object 
exclusively handles internal messages while it rewrites 
user commands in parsing messages to internal messages:
it amounts to evaluating the module expression given by the user 
to a module in the database of modules and, if successful,
to creating an internal message with the module
and with the ``from-to'' data of the parsing message.
There is an additional rule handling the case in which
the module expression in the parsing message cannot
be evaluated for a module, notifying the failure to the user.
These rules correspond to updated
versions of previously existing rules 
that handled user commands in SCC.

Rewrite rule {\tt check-sc} below specifies the creation of
an SCC proof object for
checking the sufficient completeness of a module $M$.
Here, function {\tt processSCCheck}
encapsulates the calls to functionality already available from SCC
for the sufficient completeness check,
and function {\tt createSCCProof} encapsulates the 
instantiation of the new SCC proof object and
updates to the attributes of the SCC tool object.

\begin{small}
\begin{verbatim}
 var X@SCCTool : SCCTool .   vars O O' : Oid .   var M : Module .
 var Atts : AttributeSet .   var MNReg : Map{ModuleName, Oid} .

 crl [check-sc] :
   < O : X@SCCTool | reg : MNReg, Atts > (to O from O' : check sc M)
   => if not isParameterized?(M) and-else not M :: STheory
      then createSCCProof(O', < O : SCCTool | reg : MNReg, Atts >, 
             processSCCheck(M))
      else < O : SCCTool | reg : MNReg, Atts > 
           (to O' from O : output(
              mfe-error('SCC 'cannot 'check 'parameterized 'modules 
                        'or 'theories. '\n)))
      fi   if not getName(M) in domain of MNReg .
\end{verbatim}
\end{small}
%
SCC operates on unparameterized modules 
with initial semantics.
If module $M$ conforms to these two constraints,
then a new SCC proof object is instantiated with the
emptiness result of the corresponding automaton. 
The registry attribute {\tt reg} of the SCC tool object
is updated with the name of module $M$ and the unique object 
identifier of the newly created proof object.
In the case that module $M$ does not conform to these
constraints,
an error message is issued to the user, no SCC proof
obligation is instantiated, and the SCC tool object
remains unchanged (this is done by a rule omitted here). 

\paragraph{\bf Dependencies.} 
The SCC tool object depends on termination and sort-decreasingness
checks by MTT and CRC tool objects. In general, tool dependencies can be resolved at instantiation,
for which the controller object provides information of the tools available in the
environment (including itself).

The SCC tool object
is instantiated by defining an {\em instantiation token} that takes
a map representing the available tools as input
and by a rewrite rule that creates the instance of the tool object
with the information provided in the map.
The map in the instantiation token
identifies a (tool) name $\textit{TN}$ with a (tool) object identifier
$O$ whenever the tool object for $\textit{TN}$ has object identifier $O$.
%The rewrite rule instantiates SCC tool object only if
%references to itself, to the controller object, 
%to a termination tool object, and to a sort-decreasingness 
%tool object are provided by the map.
Observe that this instantiation mechanism with
a map as a parameter benefits the modularity and extensibility
of MFE: if more tools become available in MFE, there is no need 
to modify the way tool objects are currently instantiated in MFE. 

A new SCC tool object is created by 
a term {\tt init-scc(}$\textit{TS}${\tt)} of sort
{\tt Configuration}, with $\textit{TS}$ a term
of sort \verb~Map{ToolName, Oid}~. 
The following rewrite rule {\tt init-scc-to} instantiates
the SCC tool object and creates a message to display.

\begin{small}
\begin{verbatim}
  op init-scc : Map{ToolName, Oid} -> Configuration .

  var TS : Map{ToolName, Oid} .

  rl [init-scc-to] :
    init-scc(TS)
    => < TS["SCC"] : SCC | 
          tools : TS,
          grammar : SCC-GRAMMAR, 
          current : null-oid, 
          index : 0, 
          reg : empty >
       (to TS["MFE"] from TS["SCC"] : output(string2qidList(scc-banner))) .
\end{verbatim}
\end{small}
%
The tool map $\textit{TS}$ is used to 
assign the object identifier to the SCC tool object, namely,
the object identifier with associated tool name {\tt "SCC"}.
Tool names are globally known and the controller is responsible 
for their uniqueness.
Since SCC proof objects do not exists when the SCC tool object is
created, attribute {\tt index} is set to value {\tt 0} and
attribute {\tt reg} is set to value {\tt empty}.
As the result of the SCC tool
object successful creation, an output message is sent to the controller object
with a welcoming message, here encoded by constant term {\tt scc-banner}.


\subsection{Making SCC Operational in MFE}

In order to make the SCC tool object operational in MFE,
it needs to be registered with the controller object
and added to the object configuration.
A unique tool name and a unique object identifier 
are required for registering the SCC tool object with
the controller object. In MFE, the string {\tt "SCC"}
is the global tool name for the SCC tool object and 
{\tt scc} its object identifier.
Therefore, the tools map in the controller object
is updated with the pair {\tt "SCC" |-> scc}.

The SCC tool object is added to
the initial configuration of MFE by means of the initialization
token {\tt init-scc($T$)}, with the updated tools map $T$.

{\small
\begin{verbatim}
  op TOOLS+SCC : -> Map{ToolName, Oid} .
  eq TOOLS+SCC = (TOOLS, "SCC" |-> scc) .

  rl [init] :
    init
    => [ nil,
         < mfe : Controller | 
            db : initialDatabase, input : nilTermList, output : nil,
            default : 'CONVERSION, current-tool : mfe, tools : TOOLS+SCC >
         ... 
         init-scc(TOOLS+SCC), 
         nil ] .
\end{verbatim}
}

